#!/bin/bash
# usage: ./count_schemas_test.sh

TEST_DIR="../test_scales"
LOG_DIR="../test_countlogs"
BYMC_DIR="/home/user/bymc/bymc"

if [ ! -d "$LOG_DIR" ]; then
    mkdir -p "$LOG_DIR"
    echo "Created log directory: $LOG_DIR"
fi

# this script is used for additional experiments of different scales
# for liveness-abraham-byz.ta. 
# please modify corresponding 'properties' and paths if testign other automata
properties=("cb0" "cb2" "cb4" "unaminity0" "nonblocking")


# loop
for spec in $TEST_DIR/*.ta 
do
    spec_name=$(basename "$spec")
    for prop in "${properties[@]}"
    do
        log_file="$LOG_DIR/count_schema_"$spec_name"_"$prop".log"
        COUNTCOMMAND="$BYMC_DIR/verify $TEST_DIR/$spec_name $prop -O schema.tech=ltl -O schema.incremental=1 -O schema.compute-nschemas=1"
        echo "start counting schemas for $prop of $spec_name"
        for ((i=1;i<2;i++)); do 
            timeout 30m $COUNTCOMMAND | tee "$log_file" 2>&1 | grep -q "linear extensions to enumerate" && break
        done
    done
done
